T:Type, c:T, i:Id. AtomFree(Type;T)  es.vartype(i;"x")  T & e@i. ("x" when e) = c 

latex

Definitions

P  Q, A & B, x:A. B(x), Prop, x. t(x), t  T, AB, 1of(t), False, {i..j}, Y, ||as||, nth_tl(n;as), P & Q, i<j, true, if b t else f fi, l[i], b, constR{$x:ut2}(T; c; i), A, false, init-p-realizable, i  j < k, hd(l), es-realizer(p), ij, @i always.P(x), e@i. P(e), tl(l), frame-p-realizable, Normal(T), {T}, as @ bs, x:A. B(x), P  Q, x(s), @i x initially v:T, @i only events in L change   x : T, P  Q

Lemmas

atom-free wf, constR wf, es-vartype wf, es-when wf, alle-at wf, implies-es-real, es-loc wf, Id wf, constR feasible, R-consistent wf, Knd wf, es-real-implies, R-sub-Rlist, Rinit wf, Rframe wf, init-p wf, es-real wf, R-sub-implies, es realizer wf, event system wf, select member, es-realizer wf, le wf, es-invariant1, init-p-implies, es-E wf, frame-p wf, normal-type wf, es-kind wf, l member decomp, append wf, l member wf